// ***** This file is automatically generated from CommonSequence.java.jpp

package daikon.inv.unary.sequence;

import daikon.*;
import daikon.inv.*;

import plume.*;

/**
 * Represents sequences of double values that contain a common subset.
 * Prints as <samp>{e1, e2, e3, ...} subset of x[]</samp>.
 **/

public class CommonFloatSequence
  extends SingleFloatSequence
{
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20030822L;

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /**
   * Boolean.  True iff CommonSequence invariants should be considered.
   **/
  public static boolean dkconfig_enabled = false;

  /**
   * Boolean.  Set to true to consider common sequences over hashcodes (pointers).
   */
  public static boolean dkconfig_hashcode_seqs = false;

  static final boolean debugCommonSequence = false;

  private int elts;

  /**
   * Null means no samples have been seen yet.
   * Empty array means intersection is empty.
   */
  /*@LazyNonNull*/
  private double [] intersect = null;

  protected CommonFloatSequence(PptSlice ppt) {
    super(ppt);
  }

  protected /*@Prototype*/ CommonFloatSequence() {
    super();
  }

  private static /*@Prototype*/ CommonFloatSequence proto;

  /** Returns the prototype invariant for CommonFloatSequence **/
  public static /*@Prototype*/ CommonFloatSequence get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ CommonFloatSequence ();
    return (proto);
  }

  /** returns whether or not this invariant is enabled **/
  public boolean enabled() {
    return dkconfig_enabled;
  }

  /**
   * Sequences of hashcode values won't be consistent and are thus
   * not printed by default.
   */
  public boolean instantiate_ok (VarInfo[] vis) {

    if (!valid_types (vis))
      return (false);

    return (dkconfig_hashcode_seqs || vis[0].file_rep_type.baseIsFloat());
  }

  /** instantiate an invariant on the specified slice **/
  protected CommonFloatSequence instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new CommonFloatSequence(slice);
  }

  // this.intersect is read-only, so don't clone it
  // public Object clone();

  public String repr() {
    return "CommonFloatSequence " + varNames() + ": "
      + "elts=\"" + elts;
  }

  private String printIntersect() {
    if (intersect==null)
      return "{}";

    String result = "{";
    for (int i=0; i<intersect.length; i++) {
      result += intersect[i];
      if (i!=intersect.length-1)
        result += ", ";
    }
    result += "}";
    return result;
  }

  public String format_using(OutputFormat format) {
    if (format == OutputFormat.DAIKON) return format_daikon();
    if (format == OutputFormat.SIMPLIFY) return format_simplify();

    return format_unimplemented(format);
  }

  public String format_daikon() {
    return (printIntersect() + " subset of " + var().name());
  }

  private String format_simplify() {
    if (intersect == null || intersect.length == 0) {
      return "(AND)";
    }
    String[] name = var().simplifyNameAndBounds();
    if (name == null) {
      return format_unimplemented(OutputFormat.SIMPLIFY);
    }
    String idx;
    if (!name[0].equals("|i|")) {
      idx = "i";
    } else {
      idx = "j";
    }
    StringBuffer pre_buf = new StringBuffer("");
    StringBuffer end_buf = new StringBuffer("");
    for (int i=0; i<intersect.length; i++) {
      pre_buf.append("(EXISTS ("+idx+i + ") (AND ");
      pre_buf.append("(>= "+idx+i + " " + name[1] + ") ");
      pre_buf.append("(<= "+idx+i + " " + name[2] + ") ");

      // Based on the class name, I originally wrote this method as if
      // the invariant represented a common subsequence between two
      // sequences (i.e. where the match was required to be in
      // order). In case an invariant like that is added in the
      // future, use the following:
//       if (i == 0)
//         pre_buf.append("(>= "+idx+i + " 0) ");
//       else if (i > 0)
//          pre_buf.append("(> "+idx+i + " "+idx+(i-1) +") ");
//       if (i == intersect.length - 1)
//         pre_buf.append("(< "+idx+i + " (select arrayLength " + name[0] + ")) ");
      pre_buf.append("(EQ (select (select elems " + name[0] + ") "+idx+i + ") "
                     + simplify_format_double(intersect[i]) + ")");
      if (i == intersect.length - 1)
        pre_buf.append(" ");
      end_buf.append("))");
    }
    pre_buf.append(end_buf);
    return pre_buf.toString();
  }

  public InvariantStatus check_modified(double[] a, int count) {
    if (a == null) {
      return InvariantStatus.FALSIFIED;
    } else if (intersect==null) {
      return InvariantStatus.NO_CHANGE;
    } else {
      for (int i = 0; i < a.length; i++) {
        if (Global.fuzzy.indexOf (intersect, a[i]) != -1) {
          return InvariantStatus.NO_CHANGE;
        }
      }
      return InvariantStatus.FALSIFIED;
    }
  }

  public InvariantStatus add_modified(double[] a, int count) {
    // System.out.println ("common: " + ArraysMDE.toString (a));
    if (a == null) {
      return InvariantStatus.FALSIFIED;
    } else if (intersect==null) {
      intersect = a;
      return InvariantStatus.NO_CHANGE;
    }

    double[] tmp = new double[intersect.length];
    int size = 0;
    for (int i=0; i<a.length; i++) {
      // if (a[i] in intersect) && !(a[i] in tmp), add a[i] to tmp
      int ii = Global.fuzzy.indexOf (intersect, a[i]);
      if ((ii != -1) &&
        (Global.fuzzy.indexOf (ArraysMDE.subarray(tmp,0,size), a[i]) == -1)) {
        //System.out.println ("adding " + intersect[ii] + " at " + size);

        // Carefully add the existing intersect value and not a[i].  These
        // are not necessarily the same when fuzzy floating point
        // comparisons are active.
        tmp[size++] = intersect[ii];
      }
    }
    if (size==0) {
      return InvariantStatus.FALSIFIED;
    }

    intersect = ArraysMDE.subarray(tmp, 0, size);

    intersect = Intern.intern(intersect);
    elts++;
    return InvariantStatus.NO_CHANGE;
  }

  protected double computeConfidence() {
    return 1 - Math.pow(.9, elts);
  }

  public boolean isSameFormula(Invariant other) {
    assert other instanceof CommonFloatSequence;
    return true;
  }
}
